$\forall$$T$:Type, $X$:MaInterface($T$), ${\it es}$:ES, $e$:E.
\\[0ex]($\uparrow$ma{-}in{-}interface(${\it es}$;$X$;$e$)) $\Rightarrow$ (loc($e$) $\in$ ma{-}interface{-}locs($X$))